;;;============================================================
;;;
;;; Subject: Some questions used in binary
;;;         
;;;
;;;------------------------------------------------------------
;;;
;;; Jónathan Heras Vicente
;;; Beginning date: 29-10-09
;;;
;;;============================================================

#| Certification code:

(certify-book "kenzo-remove-zeros" 0 nil)

|#


(in-package "ACL2")

(include-book "dg-natural")

(include-book "binary-remove-zeros")

(set-verify-guards-eagerness 0)

;;;************************************************************
;;;
;;; Remove-final-zeros properties
;;;
;;;************************************************************

(defthm all-zeros-p-dgb->dgn-aux-1
  (implies (and (quasi-dgb-p dgop)	
		(all-zeros-p dgop))
	   (equal (dgb->dgn dgop)
		  0)))

(defthm all-zeros-p-dgb->dgn-aux-2
  (implies (and (quasi-dgb-p dgop)	
		(all-zeros-p dgop))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  0))
  :hints (("Goal" :use ((:instance remove-initial-zeros-append-0/1-b)))))

(defthm all-zeros-p-dgb->dgn
  (implies (and (quasi-dgb-p dgop)
		(all-zeros-p dgop))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
  :hints (("Goal" :use ((:instance all-zeros-p-dgb->dgn-aux-1)
			(:instance all-zeros-p-dgb->dgn-aux-2)))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-1
  (implies (and (quasi-dgb-p dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(all-zeros-p dgop))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
  :hints (("Goal" :use ((:instance all-zeros-p-dgb->dgn)))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0
  (implies (and (quasi-dgb-p dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 0))
	   (equal (dgb->dgn dgop)
		  (+ 0 (ash (dgb->dgn (cdr dgop)) 1)))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.1
  (implies (and (quasi-dgb-p dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 1))
	   (equal (dgb->dgn dgop)
		  (+ 1 (ash (dgb->dgn (cdr dgop)) 1))
		  )))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1-help
  (equal (dgb->dgn (append '(0) a))
	 (+ 0 (ash (dgb->dgn a) 1))
		  ))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1-help2
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p (cdr dgop)))
		(eql (car dgop) 0))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  (dgb->dgn (append '(0) (remove-final-zeros (cdr dgop))))
		  )) 
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance
			 dgb->dgl-remove-final-zeros-help-1/3-aux3)
			))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 0))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  (+ 0 (ash (dgb->dgn (remove-final-zeros (cdr dgop))) 1))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1-help2)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1-help
			    (a (remove-final-zeros (cdr dgop))))))))

(defthm append-1-remove-final
  (implies (and (consp dgop)
		(eql (car dgop) 1)
		(quasi-dgb-p dgop)
		(not (all-zeros-p dgop)))
	   (equal (remove-final-zeros dgop)
		  (append '(1) (remove-final-zeros (cdr dgop))))))


(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2-help
  (equal (dgb->dgn (append '(1) a))
	 (+ 1 (ash (dgb->dgn a) 1))
		  ))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2-help2
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p (cdr dgop)))
		(eql (car dgop) 1))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  (dgb->dgn (append '(1) (remove-final-zeros (cdr dgop)))))) 
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance append-1-remove-final)))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 1))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  (+ 1 (ash (dgb->dgn (remove-final-zeros (cdr dgop))) 1))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2-help2)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2-help
			    (a (remove-final-zeros (cdr dgop))))))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.a
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 0))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0)))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.b
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 1))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0)))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop)))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.a)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.b)))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		       (dgb->dgn (remove-final-zeros (cdr dgop)))))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-1)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2)))))

(defthm dgb->dgn-remove-final-zeros
  (implies (quasi-dgb-p dgop)
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
  :hints (("Goal" :in-theory (disable remove-final-zeros)
	   :induct (dgb->dgn dgop))))

;;;============================================================================

(defthm remove-initial-zeros-append
  (implies (quasi-dgb-p l1)
	   (equal (remove-initial-zeros (append l1 l2))
		  (if (all-zeros-p l1)
		      (remove-initial-zeros l2)
		      (append (remove-initial-zeros l1) l2)))))

(defthm dgb->dgn-remove-final-zeros
  (implies (quasi-dgb-p dgop)
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop)))))

;;;============================================================================
